| 翻訳と辞書 |
| E equational theorem prover ： ウィキペディア英語版 |
E theorem prover
E is a high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the ''Automated Reasoning Group'' at TU Munich.
==System==
The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation), several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.〔
E is implemented in C and portable to most UNIX dialects and the Cygwin environment.
It is available under the GNU GPL.
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』
■ウィキペディアで「E theorem prover」の詳細全文を読む
スポンサード リンク
| 翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|